Termination of the given JBC could be proven:

0 JBC
↳1 JBC2FIG (⇐)
↳2 FIGraph
↳3 FIGtoITRSProof (⇐)
↳4 ITRS
↳5 ITRStoIDPProof (⇔)
↳6 IDP
↳7 UsableRulesProof (⇔)
↳8 IDP
↳9 ItpfGraphProof (⇔)
↳10 IDP
↳11 IDPNonInfProof (⇐)
↳12 AND
    ↳13 IDP
        ↳14 IDependencyGraphProof (⇔)
        ↳15 IDP
        ↳16 IDPNonInfProof (⇐)
        ↳17 AND
            ↳18 IDP
                ↳19 IDependencyGraphProof (⇔)
                ↳20 TRUE
            ↳21 IDP
                ↳22 IDependencyGraphProof (⇔)
                ↳23 TRUE
    ↳24 IDP
        ↳25 IDependencyGraphProof (⇔)
        ↳26 IDP
        ↳27 IDPNonInfProof (⇐)
        ↳28 AND
            ↳29 IDP
                ↳30 IDependencyGraphProof (⇔)
                ↳31 TRUE
            ↳32 IDP
                ↳33 IDependencyGraphProof (⇔)
                ↳34 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
No human-readable program information known.

Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: PastaC11

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 230 nodes with 1 SCC.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Obligation:

ITRS problem:

The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load974(java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161) → Load974ARR1(java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147)))
Load974ARR1(java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147))) → Cond_Load974ARR1(i140 > 0 && i140 < i2 && i165 >= 0 && i140 + 1 > 0, java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147))) → Load974(java.lang.Object(ARRAY(i2, a862data)), i140 + 1, i165 + -1, i260)
Load974(java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171) → Cond_Load974(i171 >= 0 && i166 < 0, java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171)
Cond_Load974(TRUE, java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171) → Load974(java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171 + -1)
The set Q consists of the following terms:
Load974(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load974ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)

(5) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(6) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


The ITRS R consists of the following rules:
Load974(java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161) → Load974ARR1(java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147)))
Load974ARR1(java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147))) → Cond_Load974ARR1(i140 > 0 && i140 < i2 && i165 >= 0 && i140 + 1 > 0, java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147))) → Load974(java.lang.Object(ARRAY(i2, a862data)), i140 + 1, i165 + -1, i260)
Load974(java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171) → Cond_Load974(i171 >= 0 && i166 < 0, java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171)
Cond_Load974(TRUE, java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171) → Load974(java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171 + -1)

The integer pair graph contains the following rules and edges:
(0): LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0]) → LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))
(1): LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1]))) → COND_LOAD974ARR1(i140[1] > 0 && i140[1] < i2[1] && i165[1] >= 0 && i140[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))
(2): COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2], i165[2], i161[2], java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2]))) → LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2] + 1, i165[2] + -1, i260[2])
(3): LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(i171[3] >= 0 && i166[3] < 0, java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])
(4): COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4] + -1)

(0) -> (1), if ((java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])) →* java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))∧(i140[0] →* i140[1])∧(java.lang.Object(ARRAY(i2[0], a862data[0])) →* java.lang.Object(ARRAY(i2[1], a862data[1])))∧(i161[0] →* i161[1])∧(i165[0] →* i165[1]))


(1) -> (2), if ((java.lang.Object(ARRAY(i2[1], a862data[1])) →* java.lang.Object(ARRAY(i2[2], a862data[2])))∧(i161[1] →* i161[2])∧(java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])) →* java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2])))∧(i165[1] →* i165[2])∧(i140[1] →* i140[2])∧(i140[1] > 0 && i140[1] < i2[1] && i165[1] >= 0 && i140[1] + 1 > 0 →* TRUE))


(2) -> (0), if ((i140[2] + 1 →* i140[0])∧(i165[2] + -1 →* i165[0])∧(i260[2] →* i161[0])∧(java.lang.Object(ARRAY(i2[2], a862data[2])) →* java.lang.Object(ARRAY(i2[0], a862data[0]))))


(2) -> (3), if ((java.lang.Object(ARRAY(i2[2], a862data[2])) →* java.lang.Object(ARRAY(i2[3], a862data[3])))∧(i140[2] + 1 →* i140[3])∧(i165[2] + -1 →* i166[3])∧(i260[2] →* i171[3]))


(3) -> (4), if ((i166[3] →* i166[4])∧(java.lang.Object(ARRAY(i2[3], a862data[3])) →* java.lang.Object(ARRAY(i2[4], a862data[4])))∧(i171[3] →* i171[4])∧(i171[3] >= 0 && i166[3] < 0 →* TRUE)∧(i140[3] →* i140[4]))


(4) -> (0), if ((i166[4] →* i165[0])∧(i140[4] →* i140[0])∧(java.lang.Object(ARRAY(i2[4], a862data[4])) →* java.lang.Object(ARRAY(i2[0], a862data[0])))∧(i171[4] + -1 →* i161[0]))


(4) -> (3), if ((i166[4] →* i166[3])∧(i171[4] + -1 →* i171[3])∧(i140[4] →* i140[3])∧(java.lang.Object(ARRAY(i2[4], a862data[4])) →* java.lang.Object(ARRAY(i2[3], a862data[3]))))



The set Q consists of the following terms:
Load974(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load974ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)

(7) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(8) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0]) → LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))
(1): LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1]))) → COND_LOAD974ARR1(i140[1] > 0 && i140[1] < i2[1] && i165[1] >= 0 && i140[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))
(2): COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2], i165[2], i161[2], java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2]))) → LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2] + 1, i165[2] + -1, i260[2])
(3): LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(i171[3] >= 0 && i166[3] < 0, java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])
(4): COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4] + -1)

(0) -> (1), if ((java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])) →* java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))∧(i140[0] →* i140[1])∧(java.lang.Object(ARRAY(i2[0], a862data[0])) →* java.lang.Object(ARRAY(i2[1], a862data[1])))∧(i161[0] →* i161[1])∧(i165[0] →* i165[1]))


(1) -> (2), if ((java.lang.Object(ARRAY(i2[1], a862data[1])) →* java.lang.Object(ARRAY(i2[2], a862data[2])))∧(i161[1] →* i161[2])∧(java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])) →* java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2])))∧(i165[1] →* i165[2])∧(i140[1] →* i140[2])∧(i140[1] > 0 && i140[1] < i2[1] && i165[1] >= 0 && i140[1] + 1 > 0 →* TRUE))


(2) -> (0), if ((i140[2] + 1 →* i140[0])∧(i165[2] + -1 →* i165[0])∧(i260[2] →* i161[0])∧(java.lang.Object(ARRAY(i2[2], a862data[2])) →* java.lang.Object(ARRAY(i2[0], a862data[0]))))


(2) -> (3), if ((java.lang.Object(ARRAY(i2[2], a862data[2])) →* java.lang.Object(ARRAY(i2[3], a862data[3])))∧(i140[2] + 1 →* i140[3])∧(i165[2] + -1 →* i166[3])∧(i260[2] →* i171[3]))


(3) -> (4), if ((i166[3] →* i166[4])∧(java.lang.Object(ARRAY(i2[3], a862data[3])) →* java.lang.Object(ARRAY(i2[4], a862data[4])))∧(i171[3] →* i171[4])∧(i171[3] >= 0 && i166[3] < 0 →* TRUE)∧(i140[3] →* i140[4]))


(4) -> (0), if ((i166[4] →* i165[0])∧(i140[4] →* i140[0])∧(java.lang.Object(ARRAY(i2[4], a862data[4])) →* java.lang.Object(ARRAY(i2[0], a862data[0])))∧(i171[4] + -1 →* i161[0]))


(4) -> (3), if ((i166[4] →* i166[3])∧(i171[4] + -1 →* i171[3])∧(i140[4] →* i140[3])∧(java.lang.Object(ARRAY(i2[4], a862data[4])) →* java.lang.Object(ARRAY(i2[3], a862data[3]))))



The set Q consists of the following terms:
Load974(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load974ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)

(9) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

(10) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0]) → LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))
(1): LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1]))) → COND_LOAD974ARR1(i140[1] > 0 && i140[1] < i2[1] && i165[1] >= 0 && i140[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))
(2): COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2], i165[2], i161[2], java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2]))) → LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2] + 1, i165[2] + -1, i260[2])
(3): LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(i171[3] >= 0 && i166[3] < 0, java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])
(4): COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4] + -1)

(0) -> (1), if (((i260[0] →* i260[1])∧(i259[0] →* i259[1])∧(i261[0] →* i261[1])∧(a1147[0] →* a1147[1]))∧(i140[0] →* i140[1])∧((i2[0] →* i2[1])∧(a862data[0] →* a862data[1]))∧(i161[0] →* i161[1])∧(i165[0] →* i165[1]))


(1) -> (2), if (((i2[1] →* i2[2])∧(a862data[1] →* a862data[2]))∧(i161[1] →* i161[2])∧((i260[1] →* i260[2])∧(i259[1] →* i259[2])∧(i261[1] →* i261[2])∧(a1147[1] →* a1147[2]))∧(i165[1] →* i165[2])∧(i140[1] →* i140[2])∧(i140[1] > 0 && i140[1] < i2[1] && i165[1] >= 0 && i140[1] + 1 > 0 →* TRUE))


(2) -> (0), if ((i140[2] + 1 →* i140[0])∧(i165[2] + -1 →* i165[0])∧(i260[2] →* i161[0])∧((i2[2] →* i2[0])∧(a862data[2] →* a862data[0])))


(2) -> (3), if (((i2[2] →* i2[3])∧(a862data[2] →* a862data[3]))∧(i140[2] + 1 →* i140[3])∧(i165[2] + -1 →* i166[3])∧(i260[2] →* i171[3]))


(3) -> (4), if ((i166[3] →* i166[4])∧((i2[3] →* i2[4])∧(a862data[3] →* a862data[4]))∧(i171[3] →* i171[4])∧(i171[3] >= 0 && i166[3] < 0 →* TRUE)∧(i140[3] →* i140[4]))


(4) -> (0), if ((i166[4] →* i165[0])∧(i140[4] →* i140[0])∧((i2[4] →* i2[0])∧(a862data[4] →* a862data[0]))∧(i171[4] + -1 →* i161[0]))


(4) -> (3), if ((i166[4] →* i166[3])∧(i171[4] + -1 →* i171[3])∧(i140[4] →* i140[3])∧((i2[4] →* i2[3])∧(a862data[4] →* a862data[3])))



The set Q consists of the following terms:
Load974(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load974ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)

(11) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair LOAD974(java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161) → LOAD974ARR1(java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147))) the following chains were created:
  • We consider the chain LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1]))) → COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1]))), COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2], i165[2], i161[2], java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2]))) → LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2]), LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0]) → LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0]))) which results in the following constraint:

    (1)    (i2[1]=i2[2]∧a862data[1]=a862data[2]∧i161[1]=i161[2]∧i260[1]=i260[2]∧i259[1]=i259[2]∧i261[1]=i261[2]∧a1147[1]=a1147[2]∧i165[1]=i165[2]∧i140[1]=i140[2]∧&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0))=TRUE∧+(i140[2], 1)=i140[0]∧+(i165[2], -1)=i165[0]∧i260[2]=i161[0]∧i2[2]=i2[0]∧a862data[2]=a862data[0] ⇒ LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0])≥NonInfC∧LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0])≥LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))∧(UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥))



    We simplified constraint (1) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (2)    (>(+(i140[1], 1), 0)=TRUE∧>=(i165[1], 0)=TRUE∧>(i140[1], 0)=TRUE∧<(i140[1], i2[1])=TRUE ⇒ LOAD974(java.lang.Object(ARRAY(i2[1], a862data[1])), +(i140[1], 1), +(i165[1], -1), i260[1])≥NonInfC∧LOAD974(java.lang.Object(ARRAY(i2[1], a862data[1])), +(i140[1], 1), +(i165[1], -1), i260[1])≥LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), +(i140[1], 1), +(i165[1], -1), i260[1], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))∧(UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i140[1] + [bni_19]i2[1] ≥ 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i140[1] + [bni_19]i2[1] ≥ 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i140[1] + [bni_19]i2[1] ≥ 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (6)    (i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i140[1] + [bni_19]i2[1] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (7)    ([1] + i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] ≥ 0∧i2[1] + [-2] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧0 = 0∧0 = 0∧[(-2)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i140[1] + [bni_19]i2[1] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (8)    ([1] + i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] ≥ 0∧i2[1] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_19] + [bni_19]i2[1] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)



  • We consider the chain LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]), COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1)), LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0]) → LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0]))) which results in the following constraint:

    (9)    (i166[3]=i166[4]∧i2[3]=i2[4]∧a862data[3]=a862data[4]∧i171[3]=i171[4]∧&&(>=(i171[3], 0), <(i166[3], 0))=TRUE∧i140[3]=i140[4]∧i166[4]=i165[0]∧i140[4]=i140[0]∧i2[4]=i2[0]∧a862data[4]=a862data[0]∧+(i171[4], -1)=i161[0] ⇒ LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0])≥NonInfC∧LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0])≥LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))∧(UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥))



    We simplified constraint (9) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:

    (10)    (>=(i171[3], 0)=TRUE∧<(i166[3], 0)=TRUE ⇒ LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], +(i171[3], -1))≥NonInfC∧LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], +(i171[3], -1))≥LOAD974ARR1(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], +(i171[3], -1), java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))∧(UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥))



    We simplified constraint (10) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (11)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧[(-1)Bound*bni_19] + [(-1)bni_19]i140[3] + [bni_19]i2[3] ≥ 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (11) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (12)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧[(-1)Bound*bni_19] + [(-1)bni_19]i140[3] + [bni_19]i2[3] ≥ 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (12) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (13)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧[(-1)Bound*bni_19] + [(-1)bni_19]i140[3] + [bni_19]i2[3] ≥ 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (13) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (14)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧[(-1)bni_19] = 0∧0 = 0∧[bni_19] = 0∧[(-1)Bound*bni_19] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (15)    (i171[3] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧[(-1)bni_19] = 0∧0 = 0∧[bni_19] = 0∧[(-1)Bound*bni_19] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)







For Pair LOAD974ARR1(java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147))) → COND_LOAD974ARR1(&&(&&(&&(>(i140, 0), <(i140, i2)), >=(i165, 0)), >(+(i140, 1), 0)), java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147))) the following chains were created:
  • We consider the chain LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1]))) → COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1]))), COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2], i165[2], i161[2], java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2]))) → LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2]) which results in the following constraint:

    (16)    (i2[1]=i2[2]∧a862data[1]=a862data[2]∧i161[1]=i161[2]∧i260[1]=i260[2]∧i259[1]=i259[2]∧i261[1]=i261[2]∧a1147[1]=a1147[2]∧i165[1]=i165[2]∧i140[1]=i140[2]∧&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0))=TRUE ⇒ LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))≥NonInfC∧LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))≥COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))∧(UIncreasing(COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))), ≥))



    We simplified constraint (16) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (17)    (>(+(i140[1], 1), 0)=TRUE∧>=(i165[1], 0)=TRUE∧>(i140[1], 0)=TRUE∧<(i140[1], i2[1])=TRUE ⇒ LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))≥NonInfC∧LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))≥COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))∧(UIncreasing(COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))), ≥))



    We simplified constraint (17) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (18)    (i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))), ≥)∧[(-1)Bound*bni_21] + [(-1)bni_21]i140[1] + [bni_21]i2[1] ≥ 0∧[(-1)bso_22] ≥ 0)



    We simplified constraint (18) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (19)    (i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))), ≥)∧[(-1)Bound*bni_21] + [(-1)bni_21]i140[1] + [bni_21]i2[1] ≥ 0∧[(-1)bso_22] ≥ 0)



    We simplified constraint (19) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (20)    (i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))), ≥)∧[(-1)Bound*bni_21] + [(-1)bni_21]i140[1] + [bni_21]i2[1] ≥ 0∧[(-1)bso_22] ≥ 0)



    We simplified constraint (20) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (21)    (i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_21] + [(-1)bni_21]i140[1] + [bni_21]i2[1] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)



    We simplified constraint (21) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (22)    ([1] + i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] ≥ 0∧i2[1] + [-2] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_21 + (-1)bni_21] + [(-1)bni_21]i140[1] + [bni_21]i2[1] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)



    We simplified constraint (22) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (23)    ([1] + i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] ≥ 0∧i2[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_21 + bni_21] + [bni_21]i2[1] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)







For Pair COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147))) → LOAD974(java.lang.Object(ARRAY(i2, a862data)), +(i140, 1), +(i165, -1), i260) the following chains were created:
  • We consider the chain LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0]) → LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0]))), LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1]))) → COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1]))), COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2], i165[2], i161[2], java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2]))) → LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2]) which results in the following constraint:

    (24)    (i260[0]=i260[1]∧i259[0]=i259[1]∧i261[0]=i261[1]∧a1147[0]=a1147[1]∧i140[0]=i140[1]∧i2[0]=i2[1]∧a862data[0]=a862data[1]∧i161[0]=i161[1]∧i165[0]=i165[1]∧i2[1]=i2[2]∧a862data[1]=a862data[2]∧i161[1]=i161[2]∧i260[1]=i260[2]∧i259[1]=i259[2]∧i261[1]=i261[2]∧a1147[1]=a1147[2]∧i165[1]=i165[2]∧i140[1]=i140[2]∧&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0))=TRUE ⇒ COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2], i165[2], i161[2], java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2])))≥NonInfC∧COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2], i165[2], i161[2], java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2])))≥LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2])∧(UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2])), ≥))



    We simplified constraint (24) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:

    (25)    (>(+(i140[1], 1), 0)=TRUE∧>=(i165[1], 0)=TRUE∧>(i140[1], 0)=TRUE∧<(i140[1], i2[1])=TRUE ⇒ COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[1], a862data[0])), i140[1], i165[1], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))≥NonInfC∧COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[1], a862data[0])), i140[1], i165[1], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))≥LOAD974(java.lang.Object(ARRAY(i2[1], a862data[0])), +(i140[1], 1), +(i165[1], -1), i260[0])∧(UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2])), ≥))



    We simplified constraint (25) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (26)    (i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2])), ≥)∧[(-1)Bound*bni_23] + [(-1)bni_23]i140[1] + [bni_23]i2[1] ≥ 0∧[1 + (-1)bso_24] ≥ 0)



    We simplified constraint (26) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (27)    (i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2])), ≥)∧[(-1)Bound*bni_23] + [(-1)bni_23]i140[1] + [bni_23]i2[1] ≥ 0∧[1 + (-1)bso_24] ≥ 0)



    We simplified constraint (27) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (28)    (i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2])), ≥)∧[(-1)Bound*bni_23] + [(-1)bni_23]i140[1] + [bni_23]i2[1] ≥ 0∧[1 + (-1)bso_24] ≥ 0)



    We simplified constraint (28) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (29)    (i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_23] + [(-1)bni_23]i140[1] + [bni_23]i2[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_24] ≥ 0)



    We simplified constraint (29) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (30)    ([1] + i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] ≥ 0∧i2[1] + [-2] + [-1]i140[1] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_23 + (-1)bni_23] + [(-1)bni_23]i140[1] + [bni_23]i2[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_24] ≥ 0)



    We simplified constraint (30) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (31)    ([1] + i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] ≥ 0∧i2[1] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_23 + bni_23] + [bni_23]i2[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_24] ≥ 0)







For Pair LOAD974(java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171) → COND_LOAD974(&&(>=(i171, 0), <(i166, 0)), java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171) the following chains were created:
  • We consider the chain LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]), COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1)) which results in the following constraint:

    (32)    (i166[3]=i166[4]∧i2[3]=i2[4]∧a862data[3]=a862data[4]∧i171[3]=i171[4]∧&&(>=(i171[3], 0), <(i166[3], 0))=TRUE∧i140[3]=i140[4] ⇒ LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥NonInfC∧LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])∧(UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥))



    We simplified constraint (32) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (33)    (>=(i171[3], 0)=TRUE∧<(i166[3], 0)=TRUE ⇒ LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥NonInfC∧LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])∧(UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥))



    We simplified constraint (33) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (34)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧[(-1)Bound*bni_25] + [(-1)bni_25]i140[3] + [bni_25]i2[3] ≥ 0∧[(-1)bso_26] ≥ 0)



    We simplified constraint (34) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (35)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧[(-1)Bound*bni_25] + [(-1)bni_25]i140[3] + [bni_25]i2[3] ≥ 0∧[(-1)bso_26] ≥ 0)



    We simplified constraint (35) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (36)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧[(-1)Bound*bni_25] + [(-1)bni_25]i140[3] + [bni_25]i2[3] ≥ 0∧[(-1)bso_26] ≥ 0)



    We simplified constraint (36) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (37)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧[(-1)bni_25] = 0∧0 = 0∧[bni_25] = 0∧[(-1)Bound*bni_25] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)



    We simplified constraint (37) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (38)    (i171[3] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧[(-1)bni_25] = 0∧0 = 0∧[bni_25] = 0∧[(-1)Bound*bni_25] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)







For Pair COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171) → LOAD974(java.lang.Object(ARRAY(i2, a862data)), i140, i166, +(i171, -1)) the following chains were created:
  • We consider the chain COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2], i165[2], i161[2], java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2]))) → LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2]), LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]), COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1)) which results in the following constraint:

    (39)    (i2[2]=i2[3]∧a862data[2]=a862data[3]∧+(i140[2], 1)=i140[3]∧+(i165[2], -1)=i166[3]∧i260[2]=i171[3]∧i166[3]=i166[4]∧i2[3]=i2[4]∧a862data[3]=a862data[4]∧i171[3]=i171[4]∧&&(>=(i171[3], 0), <(i166[3], 0))=TRUE∧i140[3]=i140[4] ⇒ COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4])≥NonInfC∧COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4])≥LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))∧(UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥))



    We simplified constraint (39) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:

    (40)    (>=(i171[3], 0)=TRUE∧<(+(i165[2], -1), 0)=TRUE ⇒ COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i171[3])≥NonInfC∧COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i171[3])≥LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), +(i171[3], -1))∧(UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥))



    We simplified constraint (40) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (41)    (i171[3] ≥ 0∧[-1]i165[2] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧[(-1)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]i140[2] + [bni_27]i2[2] ≥ 0∧[(-1)bso_28] ≥ 0)



    We simplified constraint (41) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (42)    (i171[3] ≥ 0∧[-1]i165[2] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧[(-1)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]i140[2] + [bni_27]i2[2] ≥ 0∧[(-1)bso_28] ≥ 0)



    We simplified constraint (42) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (43)    (i171[3] ≥ 0∧[-1]i165[2] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧[(-1)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]i140[2] + [bni_27]i2[2] ≥ 0∧[(-1)bso_28] ≥ 0)



    We simplified constraint (43) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (44)    (i171[3] ≥ 0∧[-1]i165[2] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧[(-1)bni_27] = 0∧0 = 0∧[bni_27] = 0∧[(-1)bni_27 + (-1)Bound*bni_27] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_28] ≥ 0)



    We simplified constraint (44) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (45)    (i171[3] ≥ 0∧i165[2] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧[(-1)bni_27] = 0∧0 = 0∧[bni_27] = 0∧[(-1)bni_27 + (-1)Bound*bni_27] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_28] ≥ 0)



  • We consider the chain COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1)), LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]), COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1)) which results in the following constraint:

    (46)    (i166[4]=i166[3]∧+(i171[4], -1)=i171[3]∧i140[4]=i140[3]∧i2[4]=i2[3]∧a862data[4]=a862data[3]∧i166[3]=i166[4]1∧i2[3]=i2[4]1∧a862data[3]=a862data[4]1∧i171[3]=i171[4]1∧&&(>=(i171[3], 0), <(i166[3], 0))=TRUE∧i140[3]=i140[4]1 ⇒ COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4]1, a862data[4]1)), i140[4]1, i166[4]1, i171[4]1)≥NonInfC∧COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4]1, a862data[4]1)), i140[4]1, i166[4]1, i171[4]1)≥LOAD974(java.lang.Object(ARRAY(i2[4]1, a862data[4]1)), i140[4]1, i166[4]1, +(i171[4]1, -1))∧(UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4]1, a862data[4]1)), i140[4]1, i166[4]1, +(i171[4]1, -1))), ≥))



    We simplified constraint (46) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:

    (47)    (>=(+(i171[4], -1), 0)=TRUE∧<(i166[3], 0)=TRUE ⇒ COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[3], +(i171[4], -1))≥NonInfC∧COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[3], +(i171[4], -1))≥LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[3], +(+(i171[4], -1), -1))∧(UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4]1, a862data[4]1)), i140[4]1, i166[4]1, +(i171[4]1, -1))), ≥))



    We simplified constraint (47) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (48)    (i171[4] + [-1] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4]1, a862data[4]1)), i140[4]1, i166[4]1, +(i171[4]1, -1))), ≥)∧[(-1)Bound*bni_27] + [(-1)bni_27]i140[4] + [bni_27]i2[4] ≥ 0∧[(-1)bso_28] ≥ 0)



    We simplified constraint (48) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (49)    (i171[4] + [-1] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4]1, a862data[4]1)), i140[4]1, i166[4]1, +(i171[4]1, -1))), ≥)∧[(-1)Bound*bni_27] + [(-1)bni_27]i140[4] + [bni_27]i2[4] ≥ 0∧[(-1)bso_28] ≥ 0)



    We simplified constraint (49) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (50)    (i171[4] + [-1] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4]1, a862data[4]1)), i140[4]1, i166[4]1, +(i171[4]1, -1))), ≥)∧[(-1)Bound*bni_27] + [(-1)bni_27]i140[4] + [bni_27]i2[4] ≥ 0∧[(-1)bso_28] ≥ 0)



    We simplified constraint (50) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (51)    (i171[4] + [-1] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4]1, a862data[4]1)), i140[4]1, i166[4]1, +(i171[4]1, -1))), ≥)∧[(-1)bni_27] = 0∧0 = 0∧[bni_27] = 0∧[(-1)Bound*bni_27] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_28] ≥ 0)



    We simplified constraint (51) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (52)    (i171[4] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4]1, a862data[4]1)), i140[4]1, i166[4]1, +(i171[4]1, -1))), ≥)∧[(-1)bni_27] = 0∧0 = 0∧[bni_27] = 0∧[(-1)Bound*bni_27] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_28] ≥ 0)



    We simplified constraint (52) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (53)    (i171[4] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4]1, a862data[4]1)), i140[4]1, i166[4]1, +(i171[4]1, -1))), ≥)∧[(-1)bni_27] = 0∧0 = 0∧[bni_27] = 0∧[(-1)Bound*bni_27] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_28] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD974(java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161) → LOAD974ARR1(java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147)))
    • ([1] + i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] ≥ 0∧i2[1] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_19] + [bni_19]i2[1] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)
    • (i171[3] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))), ≥)∧[(-1)bni_19] = 0∧0 = 0∧[bni_19] = 0∧[(-1)Bound*bni_19] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)

  • LOAD974ARR1(java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147))) → COND_LOAD974ARR1(&&(&&(&&(>(i140, 0), <(i140, i2)), >=(i165, 0)), >(+(i140, 1), 0)), java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147)))
    • ([1] + i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] ≥ 0∧i2[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_21 + bni_21] + [bni_21]i2[1] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)

  • COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2, a862data)), i140, i165, i161, java.lang.Object(java.lang.String(i260, i259, i261, a1147))) → LOAD974(java.lang.Object(ARRAY(i2, a862data)), +(i140, 1), +(i165, -1), i260)
    • ([1] + i140[1] ≥ 0∧i165[1] ≥ 0∧i140[1] ≥ 0∧i2[1] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_23 + bni_23] + [bni_23]i2[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_24] ≥ 0)

  • LOAD974(java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171) → COND_LOAD974(&&(>=(i171, 0), <(i166, 0)), java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171)
    • (i171[3] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧[(-1)bni_25] = 0∧0 = 0∧[bni_25] = 0∧[(-1)Bound*bni_25] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)

  • COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2, a862data)), i140, i166, i171) → LOAD974(java.lang.Object(ARRAY(i2, a862data)), i140, i166, +(i171, -1))
    • (i171[3] ≥ 0∧i165[2] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧[(-1)bni_27] = 0∧0 = 0∧[bni_27] = 0∧[(-1)bni_27 + (-1)Bound*bni_27] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_28] ≥ 0)
    • (i171[4] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4]1, a862data[4]1)), i140[4]1, i166[4]1, +(i171[4]1, -1))), ≥)∧[(-1)bni_27] = 0∧0 = 0∧[bni_27] = 0∧[(-1)Bound*bni_27] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_28] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(LOAD974(x1, x2, x3, x4)) = [-1] + [-1]x2 + [-1]x1   
POL(java.lang.Object(x1)) = x1   
POL(ARRAY(x1, x2)) = [-1] + [-1]x1   
POL(LOAD974ARR1(x1, x2, x3, x4, x5)) = [-1] + [-1]x2 + [-1]x1   
POL(java.lang.String(x1, x2, x3, x4)) = [-1]   
POL(COND_LOAD974ARR1(x1, x2, x3, x4, x5, x6)) = [-1] + [-1]x3 + [-1]x2   
POL(&&(x1, x2)) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(<(x1, x2)) = [-1]   
POL(>=(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(1) = [1]   
POL(-1) = [-1]   
POL(COND_LOAD974(x1, x2, x3, x4, x5)) = [-1] + [-1]x3 + [-1]x2   

The following pairs are in P>:

COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2], i165[2], i161[2], java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2]))) → LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2])

The following pairs are in Pbound:

LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1]))) → COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))
COND_LOAD974ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a862data[2])), i140[2], i165[2], i161[2], java.lang.Object(java.lang.String(i260[2], i259[2], i261[2], a1147[2]))) → LOAD974(java.lang.Object(ARRAY(i2[2], a862data[2])), +(i140[2], 1), +(i165[2], -1), i260[2])

The following pairs are in P≥:

LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0]) → LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))
LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1]))) → COND_LOAD974ARR1(&&(&&(&&(>(i140[1], 0), <(i140[1], i2[1])), >=(i165[1], 0)), >(+(i140[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))
LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])
COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))

There are no usable rules.

(12) Complex Obligation (AND)

(13) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0]) → LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))
(1): LOAD974ARR1(java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1]))) → COND_LOAD974ARR1(i140[1] > 0 && i140[1] < i2[1] && i165[1] >= 0 && i140[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a862data[1])), i140[1], i165[1], i161[1], java.lang.Object(java.lang.String(i260[1], i259[1], i261[1], a1147[1])))
(3): LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(i171[3] >= 0 && i166[3] < 0, java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])
(4): COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4] + -1)

(4) -> (0), if ((i166[4] →* i165[0])∧(i140[4] →* i140[0])∧((i2[4] →* i2[0])∧(a862data[4] →* a862data[0]))∧(i171[4] + -1 →* i161[0]))


(0) -> (1), if (((i260[0] →* i260[1])∧(i259[0] →* i259[1])∧(i261[0] →* i261[1])∧(a1147[0] →* a1147[1]))∧(i140[0] →* i140[1])∧((i2[0] →* i2[1])∧(a862data[0] →* a862data[1]))∧(i161[0] →* i161[1])∧(i165[0] →* i165[1]))


(4) -> (3), if ((i166[4] →* i166[3])∧(i171[4] + -1 →* i171[3])∧(i140[4] →* i140[3])∧((i2[4] →* i2[3])∧(a862data[4] →* a862data[3])))


(3) -> (4), if ((i166[3] →* i166[4])∧((i2[3] →* i2[4])∧(a862data[3] →* a862data[4]))∧(i171[3] →* i171[4])∧(i171[3] >= 0 && i166[3] < 0 →* TRUE)∧(i140[3] →* i140[4]))



The set Q consists of the following terms:
Load974(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load974ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)

(14) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(15) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer, Boolean


R is empty.

The integer pair graph contains the following rules and edges:
(4): COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4] + -1)
(3): LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(i171[3] >= 0 && i166[3] < 0, java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])

(4) -> (3), if ((i166[4] →* i166[3])∧(i171[4] + -1 →* i171[3])∧(i140[4] →* i140[3])∧((i2[4] →* i2[3])∧(a862data[4] →* a862data[3])))


(3) -> (4), if ((i166[3] →* i166[4])∧((i2[3] →* i2[4])∧(a862data[3] →* a862data[4]))∧(i171[3] →* i171[4])∧(i171[3] >= 0 && i166[3] < 0 →* TRUE)∧(i140[3] →* i140[4]))



The set Q consists of the following terms:
Load974(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load974ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)

(16) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1)) the following chains were created:
  • We consider the chain LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]), COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1)), LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) which results in the following constraint:

    (1)    (i166[3]=i166[4]∧i2[3]=i2[4]∧a862data[3]=a862data[4]∧i171[3]=i171[4]∧&&(>=(i171[3], 0), <(i166[3], 0))=TRUE∧i140[3]=i140[4]∧i166[4]=i166[3]1∧+(i171[4], -1)=i171[3]1∧i140[4]=i140[3]1∧i2[4]=i2[3]1∧a862data[4]=a862data[3]1 ⇒ COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4])≥NonInfC∧COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4])≥LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))∧(UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥))



    We simplified constraint (1) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (2)    (>=(i171[3], 0)=TRUE∧<(i166[3], 0)=TRUE ⇒ COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥NonInfC∧COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], +(i171[3], -1))∧(UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧[(-1)Bound*bni_22] + [(2)bni_22]i171[3] + [(-1)bni_22]i166[3] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧[(-1)Bound*bni_22] + [(2)bni_22]i171[3] + [(-1)bni_22]i166[3] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧[(-1)Bound*bni_22] + [(2)bni_22]i171[3] + [(-1)bni_22]i166[3] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (6)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_22] + [(2)bni_22]i171[3] + [(-1)bni_22]i166[3] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (7)    (i171[3] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_22 + bni_22] + [(2)bni_22]i171[3] + [bni_22]i166[3] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)







For Pair LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) the following chains were created:
  • We consider the chain LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]), COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1)) which results in the following constraint:

    (8)    (i166[3]=i166[4]∧i2[3]=i2[4]∧a862data[3]=a862data[4]∧i171[3]=i171[4]∧&&(>=(i171[3], 0), <(i166[3], 0))=TRUE∧i140[3]=i140[4] ⇒ LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥NonInfC∧LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])∧(UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥))



    We simplified constraint (8) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (9)    (>=(i171[3], 0)=TRUE∧<(i166[3], 0)=TRUE ⇒ LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥NonInfC∧LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])∧(UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥))



    We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (10)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧[bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i171[3] + [(-1)bni_24]i166[3] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (11)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧[bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i171[3] + [(-1)bni_24]i166[3] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (12)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧[bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i171[3] + [(-1)bni_24]i166[3] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (13)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i171[3] + [(-1)bni_24]i166[3] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (14)    (i171[3] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i171[3] + [bni_24]i166[3] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))
    • (i171[3] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_22 + bni_22] + [(2)bni_22]i171[3] + [bni_22]i166[3] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

  • LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])
    • (i171[3] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i171[3] + [bni_24]i166[3] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = [3]   
POL(FALSE) = [3]   
POL(COND_LOAD974(x1, x2, x3, x4, x5)) = [2]x5 + [-1]x4 + [-1]x2 + [-1]x1   
POL(java.lang.Object(x1)) = [-1] + [2]x1   
POL(ARRAY(x1, x2)) = [-1]   
POL(LOAD974(x1, x2, x3, x4)) = [1] + [2]x4 + [-1]x3   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(&&(x1, x2)) = [2]   
POL(>=(x1, x2)) = [-1]   
POL(0) = 0   
POL(<(x1, x2)) = [-1]   

The following pairs are in P>:

COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))

The following pairs are in Pbound:

COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))
LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])

The following pairs are in P≥:

LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1

(17) Complex Obligation (AND)

(18) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(3): LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(i171[3] >= 0 && i166[3] < 0, java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])


The set Q consists of the following terms:
Load974(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load974ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)

(19) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(20) TRUE

(21) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:
none


R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:
Load974(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load974ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)

(22) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

(23) TRUE

(24) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD974(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0]) → LOAD974ARR1(java.lang.Object(ARRAY(i2[0], a862data[0])), i140[0], i165[0], i161[0], java.lang.Object(java.lang.String(i260[0], i259[0], i261[0], a1147[0])))
(3): LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(i171[3] >= 0 && i166[3] < 0, java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])
(4): COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4] + -1)

(4) -> (0), if ((i166[4] →* i165[0])∧(i140[4] →* i140[0])∧((i2[4] →* i2[0])∧(a862data[4] →* a862data[0]))∧(i171[4] + -1 →* i161[0]))


(4) -> (3), if ((i166[4] →* i166[3])∧(i171[4] + -1 →* i171[3])∧(i140[4] →* i140[3])∧((i2[4] →* i2[3])∧(a862data[4] →* a862data[3])))


(3) -> (4), if ((i166[3] →* i166[4])∧((i2[3] →* i2[4])∧(a862data[3] →* a862data[4]))∧(i171[3] →* i171[4])∧(i171[3] >= 0 && i166[3] < 0 →* TRUE)∧(i140[3] →* i140[4]))



The set Q consists of the following terms:
Load974(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load974ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)

(25) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(26) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer, Boolean


R is empty.

The integer pair graph contains the following rules and edges:
(4): COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4] + -1)
(3): LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(i171[3] >= 0 && i166[3] < 0, java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])

(4) -> (3), if ((i166[4] →* i166[3])∧(i171[4] + -1 →* i171[3])∧(i140[4] →* i140[3])∧((i2[4] →* i2[3])∧(a862data[4] →* a862data[3])))


(3) -> (4), if ((i166[3] →* i166[4])∧((i2[3] →* i2[4])∧(a862data[3] →* a862data[4]))∧(i171[3] →* i171[4])∧(i171[3] >= 0 && i166[3] < 0 →* TRUE)∧(i140[3] →* i140[4]))



The set Q consists of the following terms:
Load974(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load974ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)

(27) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1)) the following chains were created:
  • We consider the chain LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]), COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1)), LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) which results in the following constraint:

    (1)    (i166[3]=i166[4]∧i2[3]=i2[4]∧a862data[3]=a862data[4]∧i171[3]=i171[4]∧&&(>=(i171[3], 0), <(i166[3], 0))=TRUE∧i140[3]=i140[4]∧i166[4]=i166[3]1∧+(i171[4], -1)=i171[3]1∧i140[4]=i140[3]1∧i2[4]=i2[3]1∧a862data[4]=a862data[3]1 ⇒ COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4])≥NonInfC∧COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4])≥LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))∧(UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥))



    We simplified constraint (1) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (2)    (>=(i171[3], 0)=TRUE∧<(i166[3], 0)=TRUE ⇒ COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥NonInfC∧COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], +(i171[3], -1))∧(UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧[(-1)Bound*bni_22] + [bni_22]i171[3] + [(-1)bni_22]i166[3] ≥ 0∧[(-1)bso_23] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧[(-1)Bound*bni_22] + [bni_22]i171[3] + [(-1)bni_22]i166[3] ≥ 0∧[(-1)bso_23] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧[(-1)Bound*bni_22] + [bni_22]i171[3] + [(-1)bni_22]i166[3] ≥ 0∧[(-1)bso_23] ≥ 0)



    We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (6)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_22] + [bni_22]i171[3] + [(-1)bni_22]i166[3] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)



    We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (7)    (i171[3] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_22 + bni_22] + [bni_22]i171[3] + [bni_22]i166[3] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)







For Pair LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) the following chains were created:
  • We consider the chain LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]), COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1)) which results in the following constraint:

    (8)    (i166[3]=i166[4]∧i2[3]=i2[4]∧a862data[3]=a862data[4]∧i171[3]=i171[4]∧&&(>=(i171[3], 0), <(i166[3], 0))=TRUE∧i140[3]=i140[4] ⇒ LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥NonInfC∧LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])∧(UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥))



    We simplified constraint (8) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (9)    (>=(i171[3], 0)=TRUE∧<(i166[3], 0)=TRUE ⇒ LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥NonInfC∧LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])≥COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])∧(UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥))



    We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (10)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧[bni_24 + (-1)Bound*bni_24] + [bni_24]i171[3] + [(-1)bni_24]i166[3] ≥ 0∧[1 + (-1)bso_25] ≥ 0)



    We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (11)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧[bni_24 + (-1)Bound*bni_24] + [bni_24]i171[3] + [(-1)bni_24]i166[3] ≥ 0∧[1 + (-1)bso_25] ≥ 0)



    We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (12)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧[bni_24 + (-1)Bound*bni_24] + [bni_24]i171[3] + [(-1)bni_24]i166[3] ≥ 0∧[1 + (-1)bso_25] ≥ 0)



    We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (13)    (i171[3] ≥ 0∧[-1] + [-1]i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[bni_24 + (-1)Bound*bni_24] + [bni_24]i171[3] + [(-1)bni_24]i166[3] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_25] ≥ 0)



    We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (14)    (i171[3] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_24 + (-1)Bound*bni_24] + [bni_24]i171[3] + [bni_24]i166[3] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_25] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))
    • (i171[3] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_22 + bni_22] + [bni_22]i171[3] + [bni_22]i166[3] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)

  • LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])
    • (i171[3] ≥ 0∧i166[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_24 + (-1)Bound*bni_24] + [bni_24]i171[3] + [bni_24]i166[3] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_25] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(COND_LOAD974(x1, x2, x3, x4, x5)) = x5 + [-1]x4 + [-1]x2 + [-1]x1   
POL(java.lang.Object(x1)) = [-1] + [-1]x1   
POL(ARRAY(x1, x2)) = [-1]   
POL(LOAD974(x1, x2, x3, x4)) = [1] + x4 + [-1]x3 + [-1]x1   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(&&(x1, x2)) = 0   
POL(>=(x1, x2)) = [-1]   
POL(0) = 0   
POL(<(x1, x2)) = [-1]   

The following pairs are in P>:

LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])

The following pairs are in Pbound:

COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))
LOAD974(java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3]) → COND_LOAD974(&&(>=(i171[3], 0), <(i166[3], 0)), java.lang.Object(ARRAY(i2[3], a862data[3])), i140[3], i166[3], i171[3])

The following pairs are in P≥:

COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], +(i171[4], -1))

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(TRUE, TRUE)1 ↔ TRUE1
&&(TRUE, FALSE)1 ↔ FALSE1
&&(FALSE, TRUE)1 ↔ FALSE1
&&(FALSE, FALSE)1 ↔ FALSE1

(28) Complex Obligation (AND)

(29) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(4): COND_LOAD974(TRUE, java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4]) → LOAD974(java.lang.Object(ARRAY(i2[4], a862data[4])), i140[4], i166[4], i171[4] + -1)


The set Q consists of the following terms:
Load974(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load974ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)

(30) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(31) TRUE

(32) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:
none


R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:
Load974(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load974ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load974(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)

(33) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

(34) TRUE